Inference at * 1 
Iof proof for Lemma eqff to assert:



1. b : 
2. b = ff
  (b) 

latex

 by BoolInd 1 

latex

 1: 

 1: 1. tt = ff
 1:   (tt)
 2: 

 2: 1. ff = ff
 2:   (ff)
 .

Definitions

t  T, Unit, , tt, , ff